package quantifieurs;

import base.Atome;
import base.Formule;
import termes.Variable;
import utils.FormuleType;
import utils.Symbole;
/**
 *  Copyright (c) 1999-2011, Ecole des Mines de Nantes
 *  All rights reserved.
 *  Redistribution and use in source and binary forms, with or without
 *  modification, are permitted provided that the following conditions are met:
 *
 *      * Redistributions of source code must retain the above copyright
 *        notice, this list of conditions and the following disclaimer.
 *      * Redistributions in binary form must reproduce the above copyright
 *        notice, this list of conditions and the following disclaimer in the
 *        documentation and/or other materials provided with the distribution.
 *      * Neither the name of the Ecole des Mines de Nantes nor the
 *        names of its contributors may be used to endorse or promote products
 *        derived from this software without specific prior written permission.
 *
 *  THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND ANY
 *  EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 *  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 *  DISCLAIMED. IN NO EVENT SHALL THE REGENTS AND CONTRIBUTORS BE LIABLE FOR ANY
 *  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 *  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 *  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 *  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 *  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 *  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

/**
 * Created by IntelliJ IDEA.
 * User: njussien
 * Date: 30/11/12
 * Time: 10:40
 */
public class PourTout extends Quantification {
    public PourTout (Variable x, Formule f) {
    	this.x = x;
    	this.f = f;
    }
    
    public String toString() {
    	//return "QQ " + this.x + "," + this.f;
    	return Symbole.POUR_TOUT + " " + this.x + "," + this.f;
    }

	public Formule negation() {
		return new Existe(this.x, this.f.negation());
	}

	public Formule supprimeConnecteurs() {
		return new PourTout(x, f.supprimeConnecteurs());
	}

	public Formule descendreNegation(boolean isNegatif) {
		if(isNegatif) return this.negation().descendreNegation(false);
		return new PourTout(this.x, this.f.descendreNegation(false));
	}

	public Formule transportQuantificateurs() {
		// 1) QQ x A(y) --> A(y)
		//if (this.f.getType() == FormuleType.ATOME) {
		if (this.f.getClass() == Atome.class) {
			Atome formuleTmp = (Atome) this.f;
			if (formuleTmp.getOperandes().length == 1) {
				Variable variableTmp = (Variable) formuleTmp.getOperandes()[0];
				if (!variableTmp.egale(this.x)) {
					return formuleTmp;
				}
			}
		}
		// 2) QQ x, QQ y A(x)  -->  QQx, A(x)
		//if (this.f.getType() == FormuleType.POURTOUT){
		if (this.f.getClass() == PourTout.class){
			PourTout formuleTmp = (PourTout) this.f;
			if (!formuleTmp.x.egale(this.x)) {
				Atome formuleTmp2 = (Atome) formuleTmp.f;
				if (formuleTmp2.getOperandes().length == 1) {
					Variable variableTmp = (Variable) formuleTmp2.getOperandes()[0];
					if (variableTmp.egale(this.x)) {
						return new PourTout(variableTmp, formuleTmp2);
					} else {
						return new PourTout(formuleTmp.x, formuleTmp2);
					}
				}
			}
		}
		return this;
	}

	public boolean isSame(Formule o) {
		//if (o.getType() != FormuleType.POURTOUT) return false;
		if (o.getClass() != PourTout.class) return false;
		PourTout tmp = (PourTout)o;
		return this.f.isSame(tmp.f) && this.x.equals(tmp.x);
	}

	public Formule miseFormeClausale() {
		// TODO
		return new PourTout(this.x, this.f.miseFormeClausale());
	}

	public FormuleType getType() {
		return FormuleType.POURTOUT;
	}

	public boolean isQuantifieursInOrder(boolean aUniversel) {
		return this.f.isQuantifieursInOrder(true);
	}
}